$\forall$$A$:MsgA, $k$:Knd. ma{-}has{-}sends($A$;$k$) $\in$ Prop